Relayer TLA+ specification, connection and channel handshake datagrams #55

istoilkovska · 2020-04-15T14:33:49Z

Description

WIP for #5

Updated Relayer TLA+ specification, that in addition to client update datagrams, now handles connection and channel handshake datagrams.

The whole specification now contains five modules:

Relayer.tla (the main module)
Environment.tla
ClientHandlers.tla
ConnectionHandlers.tla
ChannelHandlers.tla

The module Relayer.tla contains the specification of the relayer algorithm.
It instantiates the module Environment.tla, which takes care of the chain logic.
The module Environment.tla extends the modules ClientHandlers.tla,
ConnectionHandlers.tla, and ChannelHandlers.tla, which contain definition of
operators that handle client, connection handshake, and channel handshake
datagrams, respectively.

The README.md file contains instructions about how to load the specification in
the TLA+ Toolbox and check the specified invariants and properties with TLC.

For contributor use:

Unit tests written
Added test to CI if applicable
Updated CHANGELOG_PENDING.md
Linked to Github issue with discussion and accepted design OR link to spec that describes this work.
Updated relevant documentation (docs/) and code comments
Re-reviewed Files changed in the Github PR explorer

adizere

Looks amazing, though I am a bit surprised by the whopping complexity. The sharing of variables across files (pendingDatagrams) makes it hard to follow. However, this problem is exacerbated on my side since I'm still getting comfortable with TLA+.

verification/spec/relayer/Environment.tla

verification/spec/relayer/Relayer.tla

verification/spec/relayer/Environment.tla

verification/spec/relayer/ConnectionHandlers.tla

verification/spec/relayer/Relayer.tla

verification/spec/relayer/Environment.tla

ancazamfir · 2020-05-13T11:23:37Z

Relay calls PendingDatagrams for each (srcChainID, dstChainID) combination in chainIDs but then inside PendingDatagrams we do both (srcChainID, dstChainID) and (dstChainID, srcChainID) so it seems we do the work twice. I think we can simplify PendingDatagrams to only build the datagrams to dstChainID.

verification/spec/relayer/Environment.tla

verification/spec/relayer/ConnectionHandlers.tla

milosevic · 2020-05-19T08:44:08Z

verification/spec/relayer/ChannelHandlers.tla

+                            /\ dgr.type = "ChanOpenInit"
+                            /\ dgr.channelID = GetChannelID(chainID)} IN
+
+    IF chanOpenInitDgrs /= {} /\ chain.connectionEnd.state /= "UNINIT"


Should it be chain.connectionEnd.channelEnd.state?

I think this check is for the state of the underlying connection, to make sure it is initiated.

Exactly, there's a line in the ICS04 handlers stating abortTransactionUnless(connection !== null) or abortTransactionUnless(connection.state === OPEN).

milosevic · 2020-05-19T08:50:06Z

verification/spec/relayer/Relayer.tla

+    \* connection datagrams from dstChainID to srcChainID 
+    LET srcConnectionDatagrams == ComputeConnectionDatagrams(dstChainID, srcChainID) IN
+    \* connection datagrams from srcChainID to dstChainID
+    LET dstConnectionDatagrams == ComputeConnectionDatagrams(srcChainID, dstChainID) IN


If I am not wrong ConnOpenInit will be created for both source and destination chain in case dstConnectionEnd.state = "UNINIT" /\ srcConnectionEnd.state = "UNINIT"? We want non-deterministically to send it only to one of the chain.

This is fixed now, we are only sending in one direction, i.e., from srcChainID to dstChainID

milosevic · 2020-05-19T08:52:05Z

verification/spec/relayer/ClientHandlers.tla

+    LET clientUpdatedChain == [
+            height |-> chain.height,
+            counterpartyClientHeight |-> IF updateClientHeights /= {}
+                                         THEN Max(updateClientHeights)


We should store all installed heights, not just the maximum height.

Indeed, installing only the maximum height violates liveness.

milosevic

Amazing work! Few comments that should probably be addressed in a separate PR:

Chain height (environment) should be increased before datagrams are processed.
Protocols should manage its state, not chain. For example, connectionEnd should not be part of the chain, but connection handshake protocol.
It might be useful to be able to have minimal relayer spec (with a very simple protocol on top) so we can check if relayer satisfies high level properties (for example eventual message delivery)
We should always have at least two correct relayer processes and adversarial relayers (probably sufficient to model as adversary network)
We probably want to be more precise with respect to management of ids. Ids are owned by the chains and then relayer need to pick right id and to try to create the corresponding client.
We probably want to model configuration based relayer, i.e., similar functionality should be modelled using constants
I am not sure if counterpartyClientHeight is the best name for this concept. We probably want to emphasise that it is light client state, but we probably only need height as part of it to model important mechanisms.
I am not sure if UpdateRelayerClients should be atomic action. I think this should
be part of the relay functionality.

ancazamfir

The spec look great!! Thanks Ilina!

ancazamfir · 2020-05-19T18:44:30Z

verification/spec/relayer/ChannelHandlers.tla

+                            /\ dgr.type = "ChanOpenInit"
+                            /\ dgr.channelID = GetChannelID(chainID)} IN
+
+    IF chanOpenInitDgrs /= {} /\ chain.connectionEnd.state /= "UNINIT"


I think this check is for the state of the underlying connection, to make sure it is initiated.

verification/spec/relayer/ChannelHandlers.tla

Co-authored-by: Adi Seredinschi <adi@informal.systems>

…nto ilina/tla_specs

verification/spec/relayer/ClientHandlers.tla

istoilkovska added 2 commits April 3, 2020 16:43

added connection datagrams

5becdb6

relayer TLA spec: connection and channel handshake datagrams

ddf311f

istoilkovska requested review from ancazamfir and romac as code owners April 15, 2020 14:33

istoilkovska changed the title ~~Ilina/tla specs~~ [WIP] Relayer TLA+ specification, connection and channel handshake datagrams Apr 15, 2020

adizere added connection I: logic Internal: related to the relaying logic I: spec Internal: related to IBC specifications labels Apr 17, 2020

adizere reviewed Apr 20, 2020

View reviewed changes

This was referenced Apr 20, 2020

Modelling the interaction between relayers and chains #50

Closed

Connection Handshake (ICS3) L2 TLA+ spec #58

Merged

adizere reviewed Apr 28, 2020

View reviewed changes

verification/spec/relayer/Environment.tla Show resolved Hide resolved

ancazamfir reviewed May 13, 2020

View reviewed changes

verification/spec/relayer/Environment.tla Outdated Show resolved Hide resolved

verification/spec/relayer/ConnectionHandlers.tla Outdated Show resolved Hide resolved

milosevic reviewed May 19, 2020

View reviewed changes

milosevic approved these changes May 19, 2020

View reviewed changes

Refactored relayerwith Anca's comments

6871445

ancazamfir approved these changes May 19, 2020

View reviewed changes

Update verification/spec/relayer/Environment.tla

9121195

Co-authored-by: Adi Seredinschi <adi@informal.systems>

adizere mentioned this pull request May 22, 2020

[WIP] Connection handshake English spec #42

Merged

6 tasks

istoilkovska added 2 commits May 22, 2020 17:20

Addressed Adi's and Zarko's comments

f1124bb

Merge branch 'ilina/tla_specs' of github.com:informalsystems/ibc-rs i…

435449c

…nto ilina/tla_specs

ancazamfir reviewed May 26, 2020

View reviewed changes

verification/spec/relayer/ClientHandlers.tla Outdated Show resolved Hide resolved

istoilkovska added 2 commits May 26, 2020 11:57

fix in ClientHandlers

cdffb64

small fix

a2e8dfd

istoilkovska merged commit 6e01704 into master May 26, 2020

istoilkovska deleted the ilina/tla_specs branch May 27, 2020 08:47

milosevic changed the title ~~[WIP] Relayer TLA+ specification, connection and channel handshake datagrams~~ Relayer TLA+ specification, connection and channel handshake datagrams Jun 2, 2020

ancazamfir added this to the 0.5-5mo milestone Jun 10, 2020

ancazamfir mentioned this pull request Jun 10, 2020

TLA+ for Relayer Algorithms #5

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Relayer TLA+ specification, connection and channel handshake datagrams #55

Relayer TLA+ specification, connection and channel handshake datagrams #55

istoilkovska commented Apr 15, 2020 •

edited

Loading

adizere left a comment

ancazamfir commented May 13, 2020

milosevic May 19, 2020 •

edited

Loading

ancazamfir May 19, 2020

istoilkovska May 20, 2020

milosevic May 19, 2020 •

edited

Loading

istoilkovska May 22, 2020

milosevic May 19, 2020

istoilkovska May 22, 2020

milosevic left a comment

ancazamfir left a comment

ancazamfir May 19, 2020

Relayer TLA+ specification, connection and channel handshake datagrams #55

Relayer TLA+ specification, connection and channel handshake datagrams #55

Conversation

istoilkovska commented Apr 15, 2020 • edited Loading

Description

adizere left a comment

Choose a reason for hiding this comment

ancazamfir commented May 13, 2020

milosevic May 19, 2020 • edited Loading

Choose a reason for hiding this comment

ancazamfir May 19, 2020

Choose a reason for hiding this comment

istoilkovska May 20, 2020

Choose a reason for hiding this comment

milosevic May 19, 2020 • edited Loading

Choose a reason for hiding this comment

istoilkovska May 22, 2020

Choose a reason for hiding this comment

milosevic May 19, 2020

Choose a reason for hiding this comment

istoilkovska May 22, 2020

Choose a reason for hiding this comment

milosevic left a comment

Choose a reason for hiding this comment

ancazamfir left a comment

Choose a reason for hiding this comment

ancazamfir May 19, 2020

Choose a reason for hiding this comment

istoilkovska commented Apr 15, 2020 •

edited

Loading

milosevic May 19, 2020 •

edited

Loading

milosevic May 19, 2020 •

edited

Loading